YES 283.488 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



HASKELL
  ↳ LR

mainModule Main
  ((readHex :: [Char ->  [(Int,[Char])]) :: [Char ->  [(Int,[Char])])

module Main where
  import qualified Prelude



Lambda Reductions:
The following Lambda expression
\ndn * radix + d

is transformed to
readInt0 radix n d = n * radix + d

The following Lambda expression
\vu77
case vu77 of
 (ds,r) → (foldl1 (readInt0 radix) (map (fromIntegral . digToIntds),r: []
 _ → []

is transformed to
readInt1 radix digToInt vu77 = 
case vu77 of
 (ds,r) → (foldl1 (readInt0 radix) (map (fromIntegral . digToIntds),r: []
 _ → []

The following Lambda expression
\vu68
case vu68 of
 (cs@(_ : _),t) → (cs,t: []
 _ → []

is transformed to
nonnull0 vu68 = 
case vu68 of
 (cs@(_ : _),t) → (cs,t: []
 _ → []

The following Lambda expression
\(_,zs)→zs

is transformed to
zs0 (_,zs) = zs

The following Lambda expression
\(ys,_)→ys

is transformed to
ys0 (ys,_) = ys



↳ HASKELL
  ↳ LR
HASKELL
      ↳ CR

mainModule Main
  ((readHex :: [Char ->  [(Int,[Char])]) :: [Char ->  [(Int,[Char])])

module Main where
  import qualified Prelude



Case Reductions:
The following Case expression
case vu77 of
 (ds,r) → (foldl1 (readInt0 radix) (map (fromIntegral . digToIntds),r: []
 _ → []

is transformed to
readInt10 radix digToInt (ds,r) = (foldl1 (readInt0 radix) (map (fromIntegral . digToIntds),r: []
readInt10 radix digToInt _ = []

The following Case expression
case vu68 of
 (cs@(_ : _),t) → (cs,t: []
 _ → []

is transformed to
nonnull00 (cs@(_ : _),t) = (cs,t: []
nonnull00 _ = []



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
HASKELL
          ↳ IFR

mainModule Main
  ((readHex :: [Char ->  [(Int,[Char])]) :: [Char ->  [(Int,[Char])])

module Main where
  import qualified Prelude



If Reductions:
The following If expression
if isUpper d then 'A' else 'a'

is transformed to
hex0 True = 'A'
hex0 False = 'a'

The following If expression
if isDigit d then fromEnum_0 else fromEnum (hex0 (isUpper d)) - 10

is transformed to
hex1 d True = fromEnum_0
hex1 d False = fromEnum (hex0 (isUpper d)) - 10



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
HASKELL
              ↳ BR

mainModule Main
  ((readHex :: [Char ->  [(Int,[Char])]) :: [Char ->  [(Int,[Char])])

module Main where
  import qualified Prelude



Replaced joker patterns by fresh variables and removed binding patterns.
Binding Reductions:
The bind variable of the following binding Pattern
cs@(vy : vz)

is replaced by the following term
vy : vz

The bind variable of the following binding Pattern
xs@(ww : wx)

is replaced by the following term
ww : wx



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
HASKELL
                  ↳ COR

mainModule Main
  ((readHex :: [Char ->  [(Int,[Char])]) :: [Char ->  [(Int,[Char])])

module Main where
  import qualified Prelude



Cond Reductions:
The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False

The following Function with conditions
span p [] = ([],[])
span p (ww : wx)
 | p ww
 = (ww : ys,zs)
 | otherwise
 = ([],ww : wx)
where 
vu43  = span p wx
ys  = ys0 vu43
ys0 (ys,wy) = ys
zs  = zs0 vu43
zs0 (wz,zs) = zs

is transformed to
span p [] = span3 p []
span p (ww : wx) = span2 p (ww : wx)

span2 p (ww : wx) = 
span1 p ww wx (p ww)
where 
span0 p ww wx True = ([],ww : wx)
span1 p ww wx True = (ww : ys,zs)
span1 p ww wx False = span0 p ww wx otherwise
vu43  = span p wx
ys  = ys0 vu43
ys0 (ys,wy) = ys
zs  = zs0 vu43
zs0 (wz,zs) = zs

span3 p [] = ([],[])
span3 xx xy = span2 xx xy



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
HASKELL
                      ↳ LetRed

mainModule Main
  ((readHex :: [Char ->  [(Int,[Char])]) :: [Char ->  [(Int,[Char])])

module Main where
  import qualified Prelude



Let/Where Reductions:
The bindings of the following Let/Where expression
span1 p ww wx (p ww)
where 
span0 p ww wx True = ([],ww : wx)
span1 p ww wx True = (ww : ys,zs)
span1 p ww wx False = span0 p ww wx otherwise
vu43  = span p wx
ys  = ys0 vu43
ys0 (ys,wy) = ys
zs  = zs0 vu43
zs0 (wz,zs) = zs

are unpacked to the following functions on top level
span2Zs0 xz yu (wz,zs) = zs

span2Vu43 xz yu = span xz yu

span2Ys xz yu = span2Ys0 xz yu (span2Vu43 xz yu)

span2Span1 xz yu p ww wx True = (ww : span2Ys xz yu,span2Zs xz yu)
span2Span1 xz yu p ww wx False = span2Span0 xz yu p ww wx otherwise

span2Ys0 xz yu (ys,wy) = ys

span2Zs xz yu = span2Zs0 xz yu (span2Vu43 xz yu)

span2Span0 xz yu p ww wx True = ([],ww : wx)

The bindings of the following Let/Where expression
readInt 16 isHexDigit hex
where 
hex d = fromEnum d - hex1 d (isDigit d)
hex0 True = 'A'
hex0 False = 'a'
hex1 d True = fromEnum_0
hex1 d False = fromEnum (hex0 (isUpper d)) - 10

are unpacked to the following functions on top level
readHexHex1 d True = fromEnum_0
readHexHex1 d False = fromEnum (readHexHex0 (isUpper d)) - 10

readHexHex d = fromEnum d - readHexHex1 d (isDigit d)

readHexHex0 True = 'A'
readHexHex0 False = 'a'



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
HASKELL
                          ↳ NumRed

mainModule Main
  ((readHex :: [Char ->  [(Int,[Char])]) :: [Char ->  [(Int,[Char])])

module Main where
  import qualified Prelude



Num Reduction: All numbers are transformed to thier corresponding representation with Pos, Neg, Succ and Zero.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
HASKELL
                              ↳ Narrow

mainModule Main
  (readHex :: [Char ->  [(Int,[Char])])

module Main where
  import qualified Prelude



Haskell To QDPs


↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
QDP
                                    ↳ QDPSizeChangeProof
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_span2Zs01(yv246, yv247, Succ(yv2480), Zero, yv250, yv251, yv252, yv253, yv254) → new_span2Zs02(yv246, yv247, Succ(yv246), Succ(yv250), yv251, yv252, yv253, yv254)
new_span2Zs05(yv246, yv247, yv251, yv252, yv253, yv254) → new_span2Zs03(yv246, yv247, Succ(yv246), Succ(yv251), yv252, yv253, yv254)
new_span2Zs04(yv246, yv247, yv250, yv251, yv252, yv253, yv254) → new_span2Zs02(yv246, yv247, Succ(yv246), Succ(yv250), yv251, yv252, yv253, yv254)
new_span2Zs01(yv246, yv247, Zero, Zero, yv250, yv251, yv252, yv253, yv254) → new_span2Zs04(yv246, yv247, yv250, yv251, yv252, yv253, yv254)
new_span2Zs010(yv456, yv457, yv461, yv462) → new_span2Zs08(yv456, yv457, Succ(yv456), Succ(yv461), yv462)
new_span2Zs02(yv332, yv333, Succ(yv3340), Zero, yv336, yv337, yv338, yv339) → new_span2Zs05(yv332, yv333, yv336, yv337, yv338, yv339)
new_span2Zs012(yv573, yv574, yv577, yv578) → new_span2Zs011(yv573, yv574)
new_span2Zs07(yv573, yv574, Succ(yv5750), Succ(yv5760), yv577, yv578) → new_span2Zs07(yv573, yv574, yv5750, yv5760, yv577, yv578)
new_span2Zs06(yv332, yv333, yv336, yv337, yv338, yv339) → new_span2Zs(yv333)
new_span2Zs013(yv641, yv642, Succ(yv6430), Succ(yv6440)) → new_span2Zs013(yv641, yv642, yv6430, yv6440)
new_span2Zs02(yv332, yv333, Zero, Zero, yv336, yv337, yv338, yv339) → new_span2Zs06(yv332, yv333, yv336, yv337, yv338, yv339)
new_span2Zs0(yv136, yv137, yv138, yv139, yv140, yv141) → new_span2Zs00(yv136, yv137, Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero))))))))))))))))))))))))))))))))))))))))))))))), Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))), yv138, yv139, yv140, yv141)
new_span2Zs011(yv332, yv333) → new_span2Zs(yv333)
new_span2Zs07(yv573, yv574, Zero, Zero, yv577, yv578) → new_span2Zs012(yv573, yv574, yv577, yv578)
new_span2Zs08(yv580, yv581, Succ(yv5820), Zero, yv584) → new_span2Zs013(yv580, yv581, Succ(yv580), Succ(yv584))
new_span2Zs08(yv580, yv581, Succ(yv5820), Succ(yv5830), yv584) → new_span2Zs08(yv580, yv581, yv5820, yv5830, yv584)
new_span2Zs01(yv246, yv247, Succ(yv2480), Succ(yv2490), yv250, yv251, yv252, yv253, yv254) → new_span2Zs01(yv246, yv247, yv2480, yv2490, yv250, yv251, yv252, yv253, yv254)
new_span2Zs08(yv580, yv581, Zero, Zero, yv584) → new_span2Zs014(yv580, yv581, yv584)
new_span2Zs014(yv580, yv581, yv584) → new_span2Zs013(yv580, yv581, Succ(yv580), Succ(yv584))
new_span2Zs03(yv456, yv457, Zero, Succ(yv4590), yv460, yv461, yv462) → new_span2Zs08(yv456, yv457, Succ(yv456), Succ(yv461), yv462)
new_span2Zs03(yv456, yv457, Succ(yv4580), Succ(yv4590), yv460, yv461, yv462) → new_span2Zs03(yv456, yv457, yv4580, yv4590, yv460, yv461, yv462)
new_span2Zs015(yv641, yv642) → new_span2Zs011(yv641, yv642)
new_span2Zs02(yv332, yv333, Zero, Succ(yv3350), yv336, yv337, yv338, yv339) → new_span2Zs(yv333)
new_span2Zs07(yv573, yv574, Zero, Succ(yv5760), yv577, yv578) → new_span2Zs011(yv573, yv574)
new_span2Zs00(Char(Succ(yv18100)), yv182, yv183, yv184, yv185, yv186, yv187, yv188) → new_span2Zs01(yv18100, yv182, yv18100, yv183, yv184, yv185, yv186, yv187, yv188)
new_span2Zs07(yv573, yv574, Succ(yv5750), Zero, yv577, yv578) → new_span2Zs010(yv573, yv574, yv577, yv578)
new_span2Zs(:(yv970, yv971)) → new_span2Zs0(yv970, yv971, Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))), Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))), Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))), Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
new_span2Zs013(yv641, yv642, Zero, Zero) → new_span2Zs015(yv641, yv642)
new_span2Zs03(yv456, yv457, Zero, Zero, yv460, yv461, yv462) → new_span2Zs09(yv456, yv457, yv460, yv461, yv462)
new_span2Zs013(yv641, yv642, Zero, Succ(yv6440)) → new_span2Zs011(yv641, yv642)
new_span2Zs02(yv332, yv333, Succ(yv3340), Succ(yv3350), yv336, yv337, yv338, yv339) → new_span2Zs02(yv332, yv333, yv3340, yv3350, yv336, yv337, yv338, yv339)
new_span2Zs09(yv456, yv457, yv460, yv461, yv462) → new_span2Zs07(yv456, yv457, Succ(yv456), Succ(yv460), yv461, yv462)
new_span2Zs01(yv246, yv247, Zero, Succ(yv2490), yv250, yv251, yv252, yv253, yv254) → new_span2Zs03(yv246, yv247, Succ(yv246), Succ(yv251), yv252, yv253, yv254)
new_span2Zs03(yv456, yv457, Succ(yv4580), Zero, yv460, yv461, yv462) → new_span2Zs07(yv456, yv457, Succ(yv456), Succ(yv460), yv461, yv462)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
QDP
                                    ↳ QDPSizeChangeProof
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primCharToInt(Succ(yv8690), Succ(yv8700)) → new_primCharToInt(yv8690, yv8700)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
QDP
                                    ↳ QDPSizeChangeProof
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primCharToInt0(Succ(yv8670), Succ(yv8680), yv869, yv870) → new_primCharToInt0(yv8670, yv8680, yv869, yv870)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
QDP
                                    ↳ QDPSizeChangeProof
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primCharToInt1(Succ(yv8610), Succ(yv8620), yv863, yv864, yv865) → new_primCharToInt1(yv8610, yv8620, yv863, yv864, yv865)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
QDP
                                    ↳ QDPSizeChangeProof
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primCharToInt2(Succ(yv8480), Succ(yv8490), yv850, yv851, yv852, yv853) → new_primCharToInt2(yv8480, yv8490, yv850, yv851, yv852, yv853)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
QDP
                                    ↳ QDPSizeChangeProof
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primCharToInt3(Succ(yv8400), Succ(yv8410), yv842, yv843, yv844, yv845, yv846) → new_primCharToInt3(yv8400, yv8410, yv842, yv843, yv844, yv845, yv846)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
QDP
                                    ↳ QDPSizeChangeProof
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primCharToInt4(Succ(yv8310), Succ(yv8320), yv833, yv834, yv835, yv836, yv837, yv838) → new_primCharToInt4(yv8310, yv8320, yv833, yv834, yv835, yv836, yv837, yv838)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
QDP
                                    ↳ QDPSizeChangeProof
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMinusNat(Succ(yv5960), Succ(yv52700)) → new_primMinusNat(yv5960, yv52700)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
QDP
                                    ↳ QDPSizeChangeProof
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(yv5970), Succ(yv52700)) → new_primPlusNat(yv5970, yv52700)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
QDP
                                    ↳ QDPSizeChangeProof
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_readHexHex1(yv788, Succ(yv7890), Succ(yv7900)) → new_readHexHex1(yv788, yv7890, yv7900)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
QDP
                                    ↳ QDPSizeChangeProof
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_readHexHex10(yv739, Succ(yv7400), Succ(yv7410), yv742) → new_readHexHex10(yv739, yv7400, yv7410, yv742)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
QDP
                                    ↳ QDPSizeChangeProof
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat(Succ(yv46500), yv464) → new_primMulNat(yv46500, yv464)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
QDP
                                    ↳ QDPSizeChangeProof
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_foldl(yv303, yv304, yv305, yv306, Succ(yv3070), Zero, yv309, yv310, yv311, yv312, yv313, ba) → new_foldl0(yv303, yv304, yv305, yv306, Succ(yv305), Succ(yv309), yv310, yv311, yv312, yv313, ba)
new_foldl13(yv633, yv634, yv635, yv636, yv639, be) → new_foldl12(yv633, yv634, yv635, yv636, Succ(yv635), Succ(yv639), be)
new_foldl12(yv690, yv691, yv692, yv693, Zero, Succ(yv6950), bf) → new_foldl10(yv690, yv691, yv692, yv693, bf)
new_foldl0(yv464, yv465, yv466, yv467, Zero, Succ(yv4690), yv470, yv471, yv472, yv473, bb) → new_foldl4(yv464, yv465, yv466, yv467, new_span2Zs1(yv467), bb)
new_foldl11(yv624, yv625, yv626, yv627, yv630, yv631, bd) → new_foldl10(yv624, yv625, yv626, yv627, bd)
new_foldl5(yv464, yv465, yv466, yv467, yv470, yv471, yv472, yv473, bb) → new_foldl4(yv464, yv465, yv466, yv467, new_span2Zs1(yv467), bb)
new_foldl6(yv624, yv625, yv626, yv627, Succ(yv6280), Zero, yv630, yv631, bd) → new_foldl9(yv624, yv625, yv626, yv627, yv630, yv631, bd)
new_foldl1(yv475, yv476, yv477, yv478, Succ(yv4790), Zero, yv481, yv482, yv483, bc) → new_foldl6(yv475, yv476, yv477, yv478, Succ(yv477), Succ(yv481), yv482, yv483, bc)
new_foldl6(yv624, yv625, yv626, yv627, Succ(yv6280), Succ(yv6290), yv630, yv631, bd) → new_foldl6(yv624, yv625, yv626, yv627, yv6280, yv6290, yv630, yv631, bd)
new_foldl(yv303, yv304, yv305, yv306, Zero, Zero, yv309, yv310, yv311, yv312, yv313, ba) → new_foldl2(yv303, yv304, yv305, yv306, yv309, yv310, yv311, yv312, yv313, ba)
new_foldl1(yv475, yv476, yv477, yv478, Succ(yv4790), Succ(yv4800), yv481, yv482, yv483, bc) → new_foldl1(yv475, yv476, yv477, yv478, yv4790, yv4800, yv481, yv482, yv483, bc)
new_foldl2(yv303, yv304, yv305, yv306, yv309, yv310, yv311, yv312, yv313, ba) → new_foldl0(yv303, yv304, yv305, yv306, Succ(yv305), Succ(yv309), yv310, yv311, yv312, yv313, ba)
new_foldl(yv303, yv304, yv305, yv306, Zero, Succ(yv3080), yv309, yv310, yv311, yv312, yv313, ba) → new_foldl1(yv303, yv304, yv305, yv306, Succ(yv305), Succ(yv310), yv311, yv312, yv313, ba)
new_foldl7(yv633, yv634, yv635, yv636, Succ(yv6370), Zero, yv639, be) → new_foldl12(yv633, yv634, yv635, yv636, Succ(yv635), Succ(yv639), be)
new_foldl1(yv475, yv476, yv477, yv478, Zero, Zero, yv481, yv482, yv483, bc) → new_foldl8(yv475, yv476, yv477, yv478, yv481, yv482, yv483, bc)
new_foldl16(yv557, yv558, yv559, yv560, yv561, yv562, yv563, yv564, yv565, bg) → new_foldl17(yv557, new_readInt0(yv557, yv558, yv559, bg), yv560, yv561, Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero))))))))))))))))))))))))))))))))))))))))))))))), Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))), yv562, yv563, yv564, yv565, bg)
new_foldl0(yv464, yv465, yv466, yv467, Succ(yv4680), Succ(yv4690), yv470, yv471, yv472, yv473, bb) → new_foldl0(yv464, yv465, yv466, yv467, yv4680, yv4690, yv470, yv471, yv472, yv473, bb)
new_foldl8(yv475, yv476, yv477, yv478, yv481, yv482, yv483, bc) → new_foldl6(yv475, yv476, yv477, yv478, Succ(yv477), Succ(yv481), yv482, yv483, bc)
new_foldl12(yv690, yv691, yv692, yv693, Succ(yv6940), Succ(yv6950), bf) → new_foldl12(yv690, yv691, yv692, yv693, yv6940, yv6950, bf)
new_foldl14(yv690, yv691, yv692, yv693, bf) → new_foldl10(yv690, yv691, yv692, yv693, bf)
new_foldl0(yv464, yv465, yv466, yv467, Succ(yv4680), Zero, yv470, yv471, yv472, yv473, bb) → new_foldl3(yv464, yv465, yv466, yv467, yv470, yv471, yv472, yv473, bb)
new_foldl15(yv464, yv465, yv527, :(yv4670, yv4671), bb) → new_foldl16(yv464, yv465, yv527, yv4670, yv4671, Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))), Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))), Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))), Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))), bb)
new_foldl12(yv690, yv691, yv692, yv693, Zero, Zero, bf) → new_foldl14(yv690, yv691, yv692, yv693, bf)
new_foldl9(yv475, yv476, yv477, yv478, yv482, yv483, bc) → new_foldl7(yv475, yv476, yv477, yv478, Succ(yv477), Succ(yv482), yv483, bc)
new_foldl7(yv633, yv634, yv635, yv636, Succ(yv6370), Succ(yv6380), yv639, be) → new_foldl7(yv633, yv634, yv635, yv636, yv6370, yv6380, yv639, be)
new_foldl1(yv475, yv476, yv477, yv478, Zero, Succ(yv4800), yv481, yv482, yv483, bc) → new_foldl7(yv475, yv476, yv477, yv478, Succ(yv477), Succ(yv482), yv483, bc)
new_foldl(yv303, yv304, yv305, yv306, Succ(yv3070), Succ(yv3080), yv309, yv310, yv311, yv312, yv313, ba) → new_foldl(yv303, yv304, yv305, yv306, yv3070, yv3080, yv309, yv310, yv311, yv312, yv313, ba)
new_foldl6(yv624, yv625, yv626, yv627, Zero, Zero, yv630, yv631, bd) → new_foldl11(yv624, yv625, yv626, yv627, yv630, yv631, bd)
new_foldl4(yv464, yv465, yv466, yv467, yv487, bb) → new_foldl15(yv464, yv465, new_pt(yv466, bb), yv467, bb)
new_foldl10(yv464, yv465, yv466, yv467, bb) → new_foldl4(yv464, yv465, yv466, yv467, new_span2Zs1(yv467), bb)
new_foldl3(yv303, yv304, yv305, yv306, yv310, yv311, yv312, yv313, ba) → new_foldl1(yv303, yv304, yv305, yv306, Succ(yv305), Succ(yv310), yv311, yv312, yv313, ba)
new_foldl17(yv200, yv210, Char(Succ(yv20200)), yv203, yv204, yv205, yv206, yv207, yv208, yv209, bh) → new_foldl(yv200, yv210, yv20200, yv203, yv20200, yv204, yv205, yv206, yv207, yv208, yv209, bh)
new_foldl0(yv464, yv465, yv466, yv467, Zero, Zero, yv470, yv471, yv472, yv473, bb) → new_foldl5(yv464, yv465, yv466, yv467, yv470, yv471, yv472, yv473, bb)
new_foldl7(yv633, yv634, yv635, yv636, Zero, Zero, yv639, be) → new_foldl13(yv633, yv634, yv635, yv636, yv639, be)
new_foldl6(yv624, yv625, yv626, yv627, Zero, Succ(yv6290), yv630, yv631, bd) → new_foldl10(yv624, yv625, yv626, yv627, bd)

The TRS R consists of the following rules:

new_span2Zs023(yv332, yv333, Zero, Succ(yv3350), yv336, yv337, yv338, yv339) → new_span2Zs025(yv332, yv333, yv336, yv337, yv338, yv339)
new_span2Zs021(yv573, yv574, Zero, Zero, yv577, yv578) → new_span2Zs022(yv573, yv574, yv577, yv578)
new_readInt0(yv464, Neg(yv4650), Neg(yv5270), ty_Int) → Neg(new_primPlusNat0(new_primMulNat0(yv4650, yv464), yv5270))
new_primCharToInt16(Succ(yv8400), Zero, yv842, yv843, yv844, yv845, yv846) → new_primCharToInt17(yv842, yv843, yv844, yv845, yv846)
new_primCharToInt6(yv792) → Pos(Succ(yv792))
new_span2Zs031(Char(Succ(yv18100)), yv182, yv183, yv184, yv185, yv186, yv187, yv188) → new_span2Zs032(yv18100, yv182, yv18100, yv183, yv184, yv185, yv186, yv187, yv188)
new_span2Zs032(yv246, yv247, Zero, Succ(yv2490), yv250, yv251, yv252, yv253, yv254) → new_span2Zs024(yv246, yv247, yv251, yv252, yv253, yv254)
new_readHexHex11(yv788, Zero, Zero) → new_readHexHex13(yv788)
new_span2Zs021(yv573, yv574, Zero, Succ(yv5760), yv577, yv578) → new_span2Zs022(yv573, yv574, yv577, yv578)
new_primMulNat0(Zero, yv464) → Zero
new_fromEnum(yv792) → new_primCharToInt6(yv792)
new_primCharToInt5new_primCharToInt6(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
new_primCharToInt10(Zero, Zero) → new_primCharToInt7
new_primCharToInt22(Zero, Zero, yv833, yv834, yv835, yv836, yv837, yv838) → new_primCharToInt21(yv833, yv834, yv835, yv836, yv837, yv838)
new_readHexHex16(yv739, Succ(yv7400), Zero, yv742) → new_readHexHex15(yv739, yv742)
new_span2Zs032(yv246, yv247, Succ(yv2480), Zero, yv250, yv251, yv252, yv253, yv254) → new_span2Zs030(yv246, yv247, yv250, yv251, yv252, yv253, yv254)
new_readInt0(yv464, yv465, yv527, ty_Integer) → error([])
new_span2Zs016(yv456, yv457, Zero, Zero, yv460, yv461, yv462) → new_span2Zs017(yv456, yv457, yv460, yv461, yv462)
new_span2Zs016(yv456, yv457, Zero, Succ(yv4590), yv460, yv461, yv462) → new_span2Zs018(yv456, yv457, yv461, yv462)
new_span2Zs018(yv456, yv457, yv461, yv462) → new_span2Zs033(yv456, yv457, Succ(yv456), Succ(yv461), yv462)
new_primCharToInt10(Succ(yv8690), Zero) → new_primCharToInt5
new_primCharToInt18(yv842, yv843, yv844, yv845, yv846) → new_primCharToInt8
new_ms(yv744, yv745) → new_primMinusInt(new_primCharToInt9(yv744, Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))), Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))), Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))), Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))), Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))), Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))), yv745)
new_span2Zs023(yv332, yv333, Succ(yv3340), Succ(yv3350), yv336, yv337, yv338, yv339) → new_span2Zs023(yv332, yv333, yv3340, yv3350, yv336, yv337, yv338, yv339)
new_span2Zs032(yv246, yv247, Succ(yv2480), Succ(yv2490), yv250, yv251, yv252, yv253, yv254) → new_span2Zs032(yv246, yv247, yv2480, yv2490, yv250, yv251, yv252, yv253, yv254)
new_readHexHex16(yv739, Zero, Succ(yv7410), yv742) → new_readHexHex12(yv739)
new_span2Zs032(yv246, yv247, Zero, Zero, yv250, yv251, yv252, yv253, yv254) → new_span2Zs030(yv246, yv247, yv250, yv251, yv252, yv253, yv254)
new_span2Zs033(yv580, yv581, Succ(yv5820), Succ(yv5830), yv584) → new_span2Zs033(yv580, yv581, yv5820, yv5830, yv584)
new_readHexHex13(yv788) → new_fromEnum(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero))))))))))))))))))))))))))))))))))))))))))))))))
new_primCharToInt10(Zero, Succ(yv8700)) → new_primCharToInt7
new_primMinusNat0(Zero, Succ(yv52700)) → Neg(Succ(yv52700))
new_span2Zs029(yv641, yv642, Succ(yv6430), Zero) → new_span2Zs034(yv641, yv642)
new_span2Zs033(yv580, yv581, Zero, Succ(yv5830), yv584) → new_span2Zs034(yv580, yv581)
new_primCharToInt14(Succ(yv8480), Succ(yv8490), yv850, yv851, yv852, yv853) → new_primCharToInt14(yv8480, yv8490, yv850, yv851, yv852, yv853)
new_primCharToInt14(Zero, Succ(yv8490), yv850, yv851, yv852, yv853) → new_primCharToInt11(yv850, yv852, yv853)
new_primCharToInt22(Succ(yv8310), Succ(yv8320), yv833, yv834, yv835, yv836, yv837, yv838) → new_primCharToInt22(yv8310, yv8320, yv833, yv834, yv835, yv836, yv837, yv838)
new_primCharToInt14(Succ(yv8480), Zero, yv850, yv851, yv852, yv853) → new_primCharToInt15(yv850, yv851, yv852, yv853)
new_span2Zs1(:(yv970, yv971)) → new_span2Zs027(yv970, yv971, Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))), Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))), Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))), Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
new_span2Zs025(yv332, yv333, yv336, yv337, yv338, yv339) → new_span2Zs019(yv332, yv333)
new_readHexHex16(yv739, Zero, Zero, yv742) → new_readHexHex15(yv739, yv742)
new_primCharToInt11(yv850, yv852, yv853) → new_primCharToInt12(Succ(yv850), Succ(yv852), yv850, yv853)
new_span2Zs031(Char(Zero), yv182, yv183, yv184, yv185, yv186, yv187, yv188) → :(Char(Zero), yv182)
new_readHexHex14(yv686, yv687, yv688) → new_readHexHex16(yv686, Succ(yv686), Succ(yv687), yv688)
new_pt(yv98, ty_Int) → new_primMinusInt0(yv98, new_readHexHex14(yv98, Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero))))))))))))))))))))))))))))))))))))))))))))))), Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
new_primCharToInt19(Zero, Succ(yv8620), yv863, yv864, yv865) → new_primCharToInt20(yv863, yv864, yv865)
new_span2Zs021(yv573, yv574, Succ(yv5750), Succ(yv5760), yv577, yv578) → new_span2Zs021(yv573, yv574, yv5750, yv5760, yv577, yv578)
new_primCharToInt16(Zero, Zero, yv842, yv843, yv844, yv845, yv846) → new_primCharToInt18(yv842, yv843, yv844, yv845, yv846)
new_span2Zs016(yv456, yv457, Succ(yv4580), Succ(yv4590), yv460, yv461, yv462) → new_span2Zs016(yv456, yv457, yv4580, yv4590, yv460, yv461, yv462)
new_span2Zs020(yv332, yv333, yv381) → yv381
new_primCharToInt12(Zero, Succ(yv8680), yv869, yv870) → new_primCharToInt5
new_primCharToInt16(Succ(yv8400), Succ(yv8410), yv842, yv843, yv844, yv845, yv846) → new_primCharToInt16(yv8400, yv8410, yv842, yv843, yv844, yv845, yv846)
new_primCharToInt7new_primCharToInt8
new_primMinusInt0(yv678, Neg(yv6810)) → Pos(new_primPlusNat0(Succ(yv678), yv6810))
new_span2Zs017(yv456, yv457, yv460, yv461, yv462) → new_span2Zs021(yv456, yv457, Succ(yv456), Succ(yv460), yv461, yv462)
new_primCharToInt19(Zero, Zero, yv863, yv864, yv865) → new_primCharToInt20(yv863, yv864, yv865)
new_primCharToInt21(yv833, yv834, yv835, yv836, yv837, yv838) → new_primCharToInt16(Succ(yv833), Succ(yv834), yv833, yv835, yv836, yv837, yv838)
new_primCharToInt17(yv833, yv835, yv836, yv837, yv838) → new_primCharToInt14(Succ(yv833), Succ(yv835), yv833, yv836, yv837, yv838)
new_readHexHex16(yv739, Succ(yv7400), Succ(yv7410), yv742) → new_readHexHex16(yv739, yv7400, yv7410, yv742)
new_span2Zs033(yv580, yv581, Succ(yv5820), Zero, yv584) → new_span2Zs028(yv580, yv581, yv584)
new_primPlusNat0(Succ(yv5970), Succ(yv52700)) → Succ(Succ(new_primPlusNat0(yv5970, yv52700)))
new_span2Zs019(yv332, yv333) → new_span2Zs020(yv332, yv333, new_span2Zs1(yv333))
new_readHexHex11(yv788, Zero, Succ(yv7900)) → new_readHexHex13(yv788)
new_span2Zs029(yv641, yv642, Zero, Zero) → new_span2Zs026(yv641, yv642)
new_span2Zs022(yv573, yv574, yv577, yv578) → new_span2Zs019(yv573, yv574)
new_span2Zs033(yv580, yv581, Zero, Zero, yv584) → new_span2Zs028(yv580, yv581, yv584)
new_primPlusNat0(Zero, Zero) → Zero
new_span2Zs1([]) → []
new_primCharToInt14(Zero, Zero, yv850, yv851, yv852, yv853) → new_primCharToInt15(yv850, yv851, yv852, yv853)
new_readInt0(yv464, Pos(yv4650), Pos(yv5270), ty_Int) → Pos(new_primPlusNat0(new_primMulNat0(yv4650, yv464), yv5270))
new_pt(yv98, ty_Integer) → error([])
new_span2Zs029(yv641, yv642, Succ(yv6430), Succ(yv6440)) → new_span2Zs029(yv641, yv642, yv6430, yv6440)
new_primCharToInt19(Succ(yv8610), Succ(yv8620), yv863, yv864, yv865) → new_primCharToInt19(yv8610, yv8620, yv863, yv864, yv865)
new_primCharToInt15(yv850, yv851, yv852, yv853) → new_primCharToInt19(Succ(yv850), Succ(yv851), yv850, yv852, yv853)
new_primMinusNat0(Succ(yv5960), Zero) → Pos(Succ(yv5960))
new_span2Zs023(yv332, yv333, Zero, Zero, yv336, yv337, yv338, yv339) → new_span2Zs025(yv332, yv333, yv336, yv337, yv338, yv339)
new_span2Zs024(yv246, yv247, yv251, yv252, yv253, yv254) → new_span2Zs016(yv246, yv247, Succ(yv246), Succ(yv251), yv252, yv253, yv254)
new_span2Zs021(yv573, yv574, Succ(yv5750), Zero, yv577, yv578) → new_span2Zs018(yv573, yv574, yv577, yv578)
new_span2Zs034(yv580, yv581) → :(Char(Succ(yv580)), yv581)
new_span2Zs026(yv641, yv642) → new_span2Zs019(yv641, yv642)
new_readHexHex12(yv739) → new_ms(yv739, Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero))))))))))
new_primMinusInt(Neg(yv7960), yv795) → Neg(new_primPlusNat0(yv7960, Succ(yv795)))
new_readHexHex11(yv788, Succ(yv7890), Succ(yv7900)) → new_readHexHex11(yv788, yv7890, yv7900)
new_primMinusInt(Pos(yv7960), yv795) → new_primMinusNat0(yv7960, Succ(yv795))
new_primMinusInt0(yv678, Pos(yv6810)) → new_primMinusNat0(Succ(yv678), yv6810)
new_primCharToInt12(Zero, Zero, yv869, yv870) → new_primCharToInt13(yv869, yv870)
new_primCharToInt19(Succ(yv8610), Zero, yv863, yv864, yv865) → new_primCharToInt11(yv863, yv864, yv865)
new_primCharToInt8new_primCharToInt6(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
new_primCharToInt13(yv869, yv870) → new_primCharToInt10(yv869, yv870)
new_primMinusNat0(Zero, Zero) → Pos(Zero)
new_readHexHex11(yv788, Succ(yv7890), Zero) → new_readHexHex12(yv788)
new_primMulNat0(Succ(yv46500), yv464) → new_primPlusNat0(new_primMulNat0(yv46500, yv464), Succ(yv464))
new_primCharToInt9(yv823, yv824, yv825, yv826, yv827, yv828, yv829) → new_primCharToInt22(Succ(yv823), Succ(yv824), yv823, yv825, yv826, yv827, yv828, yv829)
new_span2Zs016(yv456, yv457, Succ(yv4580), Zero, yv460, yv461, yv462) → new_span2Zs017(yv456, yv457, yv460, yv461, yv462)
new_primCharToInt22(Zero, Succ(yv8320), yv833, yv834, yv835, yv836, yv837, yv838) → new_primCharToInt17(yv833, yv835, yv836, yv837, yv838)
new_primCharToInt10(Succ(yv8690), Succ(yv8700)) → new_primCharToInt10(yv8690, yv8700)
new_span2Zs027(yv136, yv137, yv138, yv139, yv140, yv141) → new_span2Zs031(yv136, yv137, Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero))))))))))))))))))))))))))))))))))))))))))))))), Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))), yv138, yv139, yv140, yv141)
new_primCharToInt12(Succ(yv8670), Succ(yv8680), yv869, yv870) → new_primCharToInt12(yv8670, yv8680, yv869, yv870)
new_readInt0(yv464, Pos(yv4650), Neg(yv5270), ty_Int) → new_primMinusNat0(new_primMulNat0(yv4650, yv464), yv5270)
new_readInt0(yv464, Neg(yv4650), Pos(yv5270), ty_Int) → new_primMinusNat0(yv5270, new_primMulNat0(yv4650, yv464))
new_span2Zs029(yv641, yv642, Zero, Succ(yv6440)) → new_span2Zs026(yv641, yv642)
new_primCharToInt12(Succ(yv8670), Zero, yv869, yv870) → new_primCharToInt13(yv869, yv870)
new_readHexHex15(yv739, yv742) → new_readHexHex11(yv739, Succ(yv739), Succ(yv742))
new_span2Zs023(yv332, yv333, Succ(yv3340), Zero, yv336, yv337, yv338, yv339) → new_span2Zs024(yv332, yv333, yv336, yv337, yv338, yv339)
new_primCharToInt20(yv863, yv864, yv865) → new_primCharToInt8
new_primCharToInt16(Zero, Succ(yv8410), yv842, yv843, yv844, yv845, yv846) → new_primCharToInt18(yv842, yv843, yv844, yv845, yv846)
new_span2Zs028(yv580, yv581, yv584) → new_span2Zs029(yv580, yv581, Succ(yv580), Succ(yv584))
new_primPlusNat0(Succ(yv5970), Zero) → Succ(yv5970)
new_primPlusNat0(Zero, Succ(yv52700)) → Succ(yv52700)
new_primCharToInt22(Succ(yv8310), Zero, yv833, yv834, yv835, yv836, yv837, yv838) → new_primCharToInt21(yv833, yv834, yv835, yv836, yv837, yv838)
new_span2Zs030(yv246, yv247, yv250, yv251, yv252, yv253, yv254) → new_span2Zs023(yv246, yv247, Succ(yv246), Succ(yv250), yv251, yv252, yv253, yv254)
new_primMinusNat0(Succ(yv5960), Succ(yv52700)) → new_primMinusNat0(yv5960, yv52700)

The set Q consists of the following terms:

new_span2Zs021(x0, x1, Succ(x2), Succ(x3), x4, x5)
new_span2Zs1(:(x0, x1))
new_readInt0(x0, Pos(x1), Pos(x2), ty_Int)
new_primCharToInt19(Zero, Succ(x0), x1, x2, x3)
new_primMinusInt(Neg(x0), x1)
new_readInt0(x0, Neg(x1), Neg(x2), ty_Int)
new_primCharToInt10(Succ(x0), Succ(x1))
new_primCharToInt20(x0, x1, x2)
new_readHexHex16(x0, Zero, Zero, x1)
new_primCharToInt7
new_span2Zs032(x0, x1, Zero, Succ(x2), x3, x4, x5, x6, x7)
new_primCharToInt13(x0, x1)
new_span2Zs032(x0, x1, Zero, Zero, x2, x3, x4, x5, x6)
new_primMinusNat0(Zero, Zero)
new_readHexHex13(x0)
new_span2Zs029(x0, x1, Succ(x2), Succ(x3))
new_readInt0(x0, Pos(x1), Neg(x2), ty_Int)
new_readInt0(x0, Neg(x1), Pos(x2), ty_Int)
new_primCharToInt19(Zero, Zero, x0, x1, x2)
new_primCharToInt10(Succ(x0), Zero)
new_readHexHex16(x0, Succ(x1), Succ(x2), x3)
new_primCharToInt22(Zero, Succ(x0), x1, x2, x3, x4, x5, x6)
new_primMinusInt0(x0, Neg(x1))
new_readHexHex12(x0)
new_primCharToInt10(Zero, Succ(x0))
new_span2Zs029(x0, x1, Zero, Succ(x2))
new_span2Zs025(x0, x1, x2, x3, x4, x5)
new_span2Zs020(x0, x1, x2)
new_primCharToInt16(Zero, Succ(x0), x1, x2, x3, x4, x5)
new_primCharToInt8
new_primCharToInt16(Succ(x0), Zero, x1, x2, x3, x4, x5)
new_span2Zs034(x0, x1)
new_span2Zs016(x0, x1, Zero, Succ(x2), x3, x4, x5)
new_readHexHex16(x0, Succ(x1), Zero, x2)
new_span2Zs016(x0, x1, Succ(x2), Succ(x3), x4, x5, x6)
new_readHexHex14(x0, x1, x2)
new_span2Zs026(x0, x1)
new_span2Zs033(x0, x1, Succ(x2), Zero, x3)
new_span2Zs023(x0, x1, Succ(x2), Succ(x3), x4, x5, x6, x7)
new_primMinusNat0(Zero, Succ(x0))
new_readHexHex11(x0, Succ(x1), Zero)
new_span2Zs031(Char(Zero), x0, x1, x2, x3, x4, x5, x6)
new_primMulNat0(Zero, x0)
new_span2Zs1([])
new_primCharToInt12(Zero, Succ(x0), x1, x2)
new_pt(x0, ty_Integer)
new_span2Zs021(x0, x1, Succ(x2), Zero, x3, x4)
new_span2Zs018(x0, x1, x2, x3)
new_span2Zs023(x0, x1, Succ(x2), Zero, x3, x4, x5, x6)
new_primCharToInt12(Zero, Zero, x0, x1)
new_span2Zs029(x0, x1, Succ(x2), Zero)
new_primCharToInt14(Succ(x0), Zero, x1, x2, x3, x4)
new_span2Zs023(x0, x1, Zero, Zero, x2, x3, x4, x5)
new_primMinusInt(Pos(x0), x1)
new_pt(x0, ty_Int)
new_primCharToInt6(x0)
new_span2Zs032(x0, x1, Succ(x2), Succ(x3), x4, x5, x6, x7, x8)
new_primCharToInt16(Zero, Zero, x0, x1, x2, x3, x4)
new_primCharToInt5
new_span2Zs033(x0, x1, Zero, Zero, x2)
new_primCharToInt18(x0, x1, x2, x3, x4)
new_primCharToInt22(Succ(x0), Zero, x1, x2, x3, x4, x5, x6)
new_span2Zs033(x0, x1, Succ(x2), Succ(x3), x4)
new_span2Zs028(x0, x1, x2)
new_primCharToInt22(Succ(x0), Succ(x1), x2, x3, x4, x5, x6, x7)
new_primCharToInt19(Succ(x0), Succ(x1), x2, x3, x4)
new_primCharToInt15(x0, x1, x2, x3)
new_span2Zs016(x0, x1, Zero, Zero, x2, x3, x4)
new_readHexHex11(x0, Zero, Zero)
new_span2Zs021(x0, x1, Zero, Zero, x2, x3)
new_readHexHex11(x0, Zero, Succ(x1))
new_readHexHex16(x0, Zero, Succ(x1), x2)
new_primCharToInt9(x0, x1, x2, x3, x4, x5, x6)
new_span2Zs029(x0, x1, Zero, Zero)
new_readInt0(x0, x1, x2, ty_Integer)
new_fromEnum(x0)
new_span2Zs032(x0, x1, Succ(x2), Zero, x3, x4, x5, x6, x7)
new_readHexHex15(x0, x1)
new_span2Zs030(x0, x1, x2, x3, x4, x5, x6)
new_primCharToInt12(Succ(x0), Zero, x1, x2)
new_span2Zs021(x0, x1, Zero, Succ(x2), x3, x4)
new_primCharToInt12(Succ(x0), Succ(x1), x2, x3)
new_span2Zs022(x0, x1, x2, x3)
new_primCharToInt14(Zero, Succ(x0), x1, x2, x3, x4)
new_primCharToInt17(x0, x1, x2, x3, x4)
new_readHexHex11(x0, Succ(x1), Succ(x2))
new_span2Zs023(x0, x1, Zero, Succ(x2), x3, x4, x5, x6)
new_primCharToInt11(x0, x1, x2)
new_primPlusNat0(Zero, Zero)
new_primCharToInt22(Zero, Zero, x0, x1, x2, x3, x4, x5)
new_span2Zs019(x0, x1)
new_primCharToInt21(x0, x1, x2, x3, x4, x5)
new_primCharToInt14(Succ(x0), Succ(x1), x2, x3, x4, x5)
new_span2Zs033(x0, x1, Zero, Succ(x2), x3)
new_primMinusNat0(Succ(x0), Zero)
new_primCharToInt16(Succ(x0), Succ(x1), x2, x3, x4, x5, x6)
new_primPlusNat0(Zero, Succ(x0))
new_primMinusInt0(x0, Pos(x1))
new_span2Zs024(x0, x1, x2, x3, x4, x5)
new_span2Zs017(x0, x1, x2, x3, x4)
new_span2Zs027(x0, x1, x2, x3, x4, x5)
new_span2Zs016(x0, x1, Succ(x2), Zero, x3, x4, x5)
new_primPlusNat0(Succ(x0), Succ(x1))
new_primMulNat0(Succ(x0), x1)
new_primCharToInt10(Zero, Zero)
new_primCharToInt14(Zero, Zero, x0, x1, x2, x3)
new_ms(x0, x1)
new_primCharToInt19(Succ(x0), Zero, x1, x2, x3)
new_span2Zs031(Char(Succ(x0)), x1, x2, x3, x4, x5, x6, x7)
new_primMinusNat0(Succ(x0), Succ(x1))
new_primPlusNat0(Succ(x0), Zero)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
QDP
                                    ↳ QDPSizeChangeProof
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_foldr(yv322, yv323, yv324, Succ(yv3250), Succ(yv3260), ba) → new_foldr(yv322, yv323, yv324, yv3250, yv3260, ba)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
QDP
                                    ↳ QDPSizeChangeProof
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_foldr0(yv235, yv236, yv237, Succ(yv2380), Succ(yv2390), yv240, ba) → new_foldr0(yv235, yv236, yv237, yv2380, yv2390, yv240, ba)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
QDP
                                    ↳ QDPSizeChangeProof
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_foldr1(yv224, yv225, yv226, Succ(yv2270), Succ(yv2280), yv229, yv230, ba) → new_foldr1(yv224, yv225, yv226, yv2270, yv2280, yv229, yv230, ba)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
QDP
                                    ↳ QDPSizeChangeProof
                                  ↳ QDP
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_foldr2(yv111, yv112, yv113, Succ(yv1140), Succ(yv1150), yv116, yv117, yv118, ba) → new_foldr2(yv111, yv112, yv113, yv1140, yv1150, yv116, yv117, yv118, ba)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
QDP
                                    ↳ QDPSizeChangeProof
                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_foldr3(yv96, yv97, yv98, Succ(yv990), Succ(yv1000), yv101, yv102, yv103, yv104, ba) → new_foldr3(yv96, yv97, yv98, yv990, yv1000, yv101, yv102, yv103, yv104, ba)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ LetRed
                        ↳ HASKELL
                          ↳ NumRed
                            ↳ HASKELL
                              ↳ Narrow
                                ↳ AND
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
                                  ↳ QDP
QDP
                                    ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_foldr4(yv54, yv55, yv56, Succ(yv570), Succ(yv580), yv59, yv60, yv61, yv62, yv63, ba) → new_foldr4(yv54, yv55, yv56, yv570, yv580, yv59, yv60, yv61, yv62, yv63, ba)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: